/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import java.util.ArrayList;
import java.util.List;

import alloy.util.Dbg;
import alloy.util.Util;

/**
 * A Boolean DAG node computing an arbitrary function of its child nodes.  The function
 * is specified by a set of CNF clauses in terms of variables representing the
 * children and the function result; the CNF clauses are true iff the result
 * correctly computes the function of the children represented by this node.
 * <p>
 * In the clause set, literals 1..n represent the n children, literal n+1 represents
 * the result, and literals higher than n+1 represent auxiliary Boolean variables.
 */
class CNFFunc extends BooleanFormula {
    /** Child formulas -- represented by literals 1..n in the clauses. */
    BooleanFormula[] subexprs;

    /**
     * The CNF clauses implicitly representing the Boolean function that
     * this node computes of its children.  The clauses are true iff
     * the literal n+1 computes the correct Boolean function of the
     * literals 1..n.
     */
    List /* of int[] */  clauses = new ArrayList();

    CNFFunc(BooleanFormula[] subexprs_) {
	this.subexprs = subexprs_;
    }

    CNFFunc(BooleanFormula[] subexprs_, List /* of int[] */ clauses_) {
	this.subexprs = subexprs_;
	this.clauses = clauses_;
	// check that all literals are within valid range.
	for (int i=0; i<clauses_.size(); i++) {
	    int[] clause = (int[])clauses_.get(i);
	    Dbg.chk(clause.length > 0);
	    for (int j=0; j<clause.length; j++) {
		int lit = clause[j];
		int var = Math.abs(lit);
		Dbg.chk(var > 0 && var <= subexprs_.length + 1);
	    }
	}
    }

    /**
     * Return the variable that, in the CNF clauses, stands for the result
     * of applying this CNFFunc to its children.
     */
    int getResultVar() { return subexprs.length + 1; }
    
    protected boolean checkConstantValued() {
	for (int i=0; i<subexprs.length; i++)
	    if (!subexprs[i].isConstantValued())
		return false;
	return true;
    }

    protected Object handleVisitor(GBF_V visitor) { return visitor.forCNFFunc(this); }
    
    /** returns the # of boolean vars used by this expression */
    int getNumVars() {
	int maxVar = 0;
	for (int i=0; i<subexprs.length; i++) {
	    int mhere = subexprs[i].getNumVars();
	    if (mhere > maxVar)
		maxVar = mhere;
	}
	return maxVar;
    }

    public String toString() {
	StringBuffer sb = new StringBuffer();
	sb.append("C[");
	for (int i=0; i<clauses.size(); i++) {
	    int[] clause = (int[])clauses.get(i);
	    sb.append(Util.str(clause));
	}
	sb.append(" : ");
	for (int i=0; i<subexprs.length; i++) {
	    sb.append(subexprs[i]);
	    sb.append(" ");
	}
	sb.append("]");

	return sb.toString();
    }
}
